Nuprl Lemma : ocmon_trans
13,42
postcript
pdf
g
:OCMon,
a
,
b
,
c
:|
g
|. (
(
a
b
))
(
(
b
c
))
(
(
a
c
))
latex
Up
groups
1
Definitions
t
T
,
x
:
A
.
B
(
x
)
,
AntiSym(
T
;
x
,
y
.
R
(
x
;
y
))
,
Trans(
T
;
x
,
y
.
E
(
x
;
y
))
,
Refl(
T
;
x
,
y
.
E
(
x
;
y
))
,
Connex(
T
;
x
,
y
.
R
(
x
;
y
))
,
Order(
T
;
x
,
y
.
R
(
x
;
y
))
,
monot(
T
;
x
,
y
.
R
(
x
;
y
);
f
)
,
Cancel(
T
;
S
;
op
)
,
Linorder(
T
;
x
,
y
.
R
(
x
;
y
))
,
P
&
Q
Lemmas
ocmon
wf
,
ocmon
properties
origin
g:OCMon, a, b, c:|g|. (
(a 
b)) 
((b c)) ((a c)) g:OCMon, a, b, c:|g|. ((a b)) ((b c)) ((a c)) 
T